\begin{tabbing} $\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $A$:ecl(${\it ds}$; ${\it da}$), ${\it snd}$:msg{-}spec(${\it ds}$; ${\it da}$),\+ \\[0ex]${\it upd}$:update{-}spec(${\it ds}$; ${\it da}$), $j$:Id. \-\\[0ex]msg{-}spec{-}loc(${\it snd}$; $i$) \\[0ex]$\Rightarrow$ sqequal(R{-}has{-}loc(ecl{-}machine\{ecl:ut2\}($i$; ${\it ds}$; ${\it da}$; $A$; ${\it snd}$; ${\it upd}$); $j$); eq\_id($i$; $j$)) \end{tabbing}